$\forall$$A$, $B$:Type, ${\it eq}_{1}$:EqDecider($A$), ${\it eq}_{2}$:EqDecider($B$), $L$:($A$$\times$$B$) List. fpf($L$) $\in$ $a$:$A$ fp$\rightarrow$ $B$ List